recognizer-p(es;T;A;P;k;i;r;x)
== e@i. (kind(e) = k)  (valtype(e) r T) & (vartype(i;x) r A)
== & @i(r:)
== & e@i. (first(e))  ((r when e) = ff)
== & e@i.
== & ((r after e))  (e':E. ((e' loc e  & kind(e') = k) c ((P((x when e'),val(e')))))) 

latex

---

clarification:

recognizer-p(es;T;A;P;k;i;r;x)
== alle-at(es;i;e.(es-kind(es; e) = k  Knd)  (es-valtype(es; e) r T))
== & (es-vartype(es; i; x) r A)
== & es-dtype(es;i;r;)
== & alle-at(es;i;e.(es-first(es; e))  (es-when(es; r; e) = ff  ))
== & alle-at(es;i;e.(es-after(es; r; e))
== &  (e':es-E(es)
== &  (((es-le(es;e';e) & es-kind(es; e') = k  Knd)
== &  (c ((P(es-when(es; x; e'),es-val(es; e'))))))) 

latex

Definitions	valtype(e), vartype(i;x), @i(x:T), P  Q, first(e), , ff, e@i. P(e), P  Q, (x after e), x:A. B(x), E, A c B, P & Q, e loc e' , s = t, Knd, kind(e), b, f(a), x when e, val(e)
FDL editor aliases	recognizer-p